Metamath Blueprint : AKS (PRIMES is in P)

Extension of ring homomorphism over ring extensions

Let A \subset B be a finite ring extension. Fix a ring homomorphism F : A → C, where C is an algebraically closed field. There is a ring homomorphisms \overline{F}: B → C that extends F.